Search for: All records

Abstract Automatic Program Repair (APR) has garnered significant attention as a practical research domain focused on automatically fixing bugs in programs. While existing APR techniques primarily target imperative programming languages like C and Java, there is a growing need for effective solutions applicable to declarative software specification languages. This paper systematically investigates the capacity of Large Language Models (LLMs) to repair declarative specifications in Alloy, a declarative formal language used for software specification. We designed six different repair settings, encompassing single-agent and dual-agent paradigms, utilizing various LLMs. These configurations also incorporate different levels of feedback, including an auto-prompting mechanism for generating prompts autonomously using LLMs. Our study reveals that dual-agent with auto-prompting setup outperforms the other settings, albeit with a marginal increase in the number of iterations and token usage. This dual-agent setup demonstrated superior effectiveness compared to state-of-the-art Alloy APR techniques when evaluated on a comprehensive set of benchmarks. This work is the first to empirically evaluate LLM capabilities to repair declarative specifications, while taking into account recent trending LLM concepts such as LLM-based agents, feedback, auto-prompting, and tools, thus paving the way for future agent-based techniques in software engineering. 

Statically typed languages offer numerous benefits to developers, such as improved code quality and reduced runtime errors, but they also require the overhead of manual type annotations. To mitigate this burden, language designers have started incorporating support for type inference, where the compiler infers the type of a variable based on its declaration/usage context. As a result, type annotations are optional in certain contexts, and developers are empowered to use type inference in these situations. However, the usage patterns of type annotations in languages that support type inference are unclear. These patterns can help provide evidence for further research in program comprehension, in language design, and for education. We conduct a large-scale empirical study using Boa, a tool for mining software repositories, to investigate when and where developers use type inference in 498,963 Kotlin projects. We choose Kotlin because it is the default language for Android development, one of the largest software marketplaces. Additionally, Kotlin has supported declaration-site optional type annotations from its initial release. Our findings reveal that type inference is frequently employed for local variables and variables initialized with method calls declared outside the file are more likely to use type inference. These results have significant implications for language designers, providing valuable insight into where to allow type inference and how to optimize type inference algorithms for maximum efficiency, ultimately improving the development experience for developers. 

Cyber-physical systems interact with the world through software controlling physical effectors. Carefully designed controllers, implemented as safety-critical control software, also interact with other parts of the software suite, and may be difficult to separate, verify, or maintain. Moreover, some software changes, not intended to impact control system performance, do change controller response through a variety of means including interaction with external libraries or unmodeled changes only existing in the cyber system (e.g., exception handling). As a result, identifying safety-critical control software, its boundaries with other embedded software in the system, and the way in which control software evolves could help developers isolate, test, and verify control implementation, and improve control software development. In this work we present an automated technique, based on a novel application of machine learning, to detect commits related to control software, its changes, and how the control software evolves. We leverage messages from developers (e.g., commit comments), and code changes themselves to understand how control software is refined, extended, and adapted over time. We examine three distinct, popular, real-world, safety-critical autopilots—ArduPilot, Paparazzi UAV, and LibrePilot to test our method demonstrating an effective detection rate of 0.95 for control-related code changes.